Inference at * 1 
Iof proof for Lemma fseg select:



1. T : Type
2. l1 : T List
3. l2 : T List
4. fseg(T;l1;l2)
5. i : 
6. i < ||l1||
  l1[i] = l2[((||l2|| - ||l1||)+i)] 

latex

 by ((D (-3)) 
CollapseTHEN (StrongHypSubst (-3) 0)) 

latex

C1: 

C1: 4. L : T List
C1: 5. l2 = (L @ l1)
C1: 6. i : 
C1: 7. i < ||l1||
C1:   l1[i] = (L @ l1)[((||L @ l1|| - ||l1||)+i)]
C2: .....wf..... NILNIL

C2: 4. L : T List
C2: 5. l2 = (L @ l1)
C2: 6. i : 
C2: 7. i < ||l1||
C2: 8. z : T List
C2: 9. z = (L @ l1)
C2:   (l1[i] = z[((||z|| - ||l1||)+i)])  
C.

Definitions	fseg(T;L1;L2), x:A. B(x), x:A  B(x), , l[i], as @ bs, t  T, x:A. B(x), s = t, type List, Type, , {x:A| B(x)} , , A  B, A, False, P  Q, x:AB(x), Void, a < b, n - m, n+m, -n, ||as||
Lemmas	select wf, nat wf, member wf, le wf